(DEFPROP NCPROD (NIL (1 (5 1 NCPRODGREMLIN))) THERASING) 
(DEFPROP NPRODUCT (NIL (1 (5 1 NPRODUCTGREMLIN))) THERASING) 
(DEFPROP THVRB (NIL (2 (4 3 TAFACT TFACT ←) (5 2 TAPROD TPROD)) (3 (4 3 TAFACT TFACT ←) (5 2 TAPROD TPROD)) (4 (~
5 2 TAPROD TPROD))) THCONSE) 
(DEFPROP THVRB (NIL (2 (4 10 NVFACTGREMLIN VFACTGREMLIN NCGREMLIN CGREMLIN N=GREMLIN =GREMLIN NCFACTGREMLIN CFAC~
TGREMLIN) (5 4 NPRODUCTGREMLIN PRODUCTGREMLIN NCPRODGREMLIN CPRODGREMLIN)) (3 (4 10 NVFACTGREMLIN VFACTGREMLIN N~
CGREMLIN CGREMLIN N=GREMLIN =GREMLIN NCFACTGREMLIN CFACTGREMLIN) (5 4 NPRODUCTGREMLIN PRODUCTGREMLIN NCPRODGREML~
IN CPRODGREMLIN)) (4 (5 4 NPRODUCTGREMLIN PRODUCTGREMLIN NCPRODGREMLIN CPRODGREMLIN))) THERASING) 
(DEFPROP N= (NIL (1 (4 1 N=GREMLIN))) THERASING) 
(DEFPROP PRODUCT (NIL (1 (5 1 TAPROD))) THCONSE) 
(DEFPROP PRODUCT (NIL (1 (5 1 PRODUCTGREMLIN))) THERASING) 
(DEFPROP NC (NIL (1 (4 1 NCGREMLIN))) THERASING) 
(DEFPROP = (NIL (1 (4 1 =GREMLIN))) THERASING) 
(DEFPROP C (NIL (1 (4 1 ←))) THCONSE) 
(DEFPROP C (NIL (1 (4 1 CGREMLIN))) THERASING) 
(DEFPROP R (NIL (4 (4 3 TAFACT TFACT ←)) (5 (5 2 TAPROD TPROD))) THCONSE) 
(DEFPROP R (NIL (4 (4 10 NVFACTGREMLIN VFACTGREMLIN NCGREMLIN CGREMLIN N=GREMLIN =GREMLIN NCFACTGREMLIN CFACTGRE~
MLIN)) (5 (5 4 NPRODUCTGREMLIN PRODUCTGREMLIN NCPRODGREMLIN CPRODGREMLIN))) THERASING) 
(DEFPROP NCFACT (NIL (1 (4 1 NCFACTGREMLIN))) THERASING) 
(DEFPROP CFACT (NIL (1 (4 1 TFACT))) THCONSE) 
(DEFPROP CFACT (NIL (1 (4 1 CFACTGREMLIN))) THERASING) 
(DEFPROP NVFACT (NIL (1 (4 1 NVFACTGREMLIN))) THERASING) 
(DEFPROP VFACT (NIL (1 (4 1 TAFACT))) THCONSE) 
(DEFPROP VFACT (NIL (1 (4 1 VFACTGREMLIN))) THERASING) 
(DEFPROP CPROD (NIL (1 (5 1 TPROD))) THCONSE) 
(DEFPROP CPROD (NIL (1 (5 1 CPRODGREMLIN))) THERASING) 
(THDATA) 
((ISVAR X0)) 
((VFACT (1) (1) R)) 
((INTEGER N)) 
NIL